Conversation
jar-ben
changed the title
…ede combined view)
…of a comment change
e917f8e to
1caafbb
Compare
| """One named CVL spec buffer the agent authors. Frozen and pydantic so it is both the substrate's | ||
| algorithm type and the shape stored (serializably) in graph state.""" |
| name: str | ||
| #: The buffer's own CVL text — its rules, its ``methods{}`` block, and its ``import`` statements. |
There was a problem hiding this comment.
I assume it is an invariant that buffers[nm].name == nm for all nm?
| returned sorted by name. A run-target buffer imports a shared (``is_run_target=false``) buffer only | ||
| when it does, so a shared buffer belongs to the closure (and invalidation set) of exactly the |
There was a problem hiding this comment.
"a run target buffer imports a shared buffer only when it does"
????? what?
| return tuple(out) | ||
|
|
||
|
|
||
| def import_closure(buffers: Mapping[str, NamedBuffer], name: str) -> list[NamedBuffer]: |
There was a problem hiding this comment.
is there a reason we don't have the prover create this inventory for us? The answer might be "because it doesn't produce the output we want, and this needs to land independently of that". I buy that answer, to be clear, but I want to make sure I understand the reason.
There was a problem hiding this comment.
Exactly. I was checking it, the prover does not cheaply produce it. I am a bit worried about this too, i.e. I will add the functionality to the prover (but the integration is non-trivial (needing prover version release and bumping pointers at various places).
| (e.g. skipped-property or conf-flag markers). Editing the buffer OR any buffer it imports changes | ||
| the digest, so it keys the buffer's cached verify/review. Mirrors | ||
| :meth:`ContentCache.compute_cache_key` (content-keyed, order-independent).""" | ||
| # TODO: a pure-comment edit (e.g. reframing a property's justification docstring) changes this |
There was a problem hiding this comment.
WHAT IF WE USED THE CANONICAL TAC
There was a problem hiding this comment.
Well, you know the tac is not really deterministic, and then there is also the "how to obtain it" question. The bigger problem perhaps is that we want to, at the end, provide the user with the final artifacts (including right cvl comments).
This is a pre-existing issue. I saw in a run of AutoProver that 5-10 % of his prover runs were just due to CVL comment edits. I will look into this later (perhaps I was just unlucky with that run).
There was a problem hiding this comment.
I was just kidding in any event
| Verifying — submit / collect (buffers prove in parallel; never wait on a slow buffer to work on a fast | ||
| one): | ||
| - **Settle the shared base before submitting anything that imports it.** Submit a run-target buffer only | ||
| once BOTH (i) that buffer is finished AND (ii) every shared buffer it imports is finished — you do not |
There was a problem hiding this comment.
what does it mean for a run-target buffer to be "finished"? Like, finished editing?
| under-approximation), edit the shared buffer; that invalidates every buffer importing it — the | ||
| board lists them under `needs (re)submission` (including ones already verified) — so re-submit | ||
| each of them. |
There was a problem hiding this comment.
er, no it doesn't. This makes it sound like the board tells the agent what jobs need to be resubmitted based on the fix required for a shared spec fix. But it has no way of knowing a CEX remediation requires a shared spec fix?
| working_dir=pathlib.Path(run_root), | ||
| curr_spec=st["curr_spec"], | ||
| curr_spec=None, | ||
| prover_runner=WrappedProverRunner( |
There was a problem hiding this comment.
UH. Wait, hang on. This breaks the plugin API in a BIG way that will break some other code. let's discuss
There was a problem hiding this comment.
So, CVLAuthorState now exposes the buffer set directly (buffers: Mapping[str, NamedBuffer]) plus spec_for_rule(rule) -> str | None, which returns the CVL for the buffer that declares that rule (its text + transitive imports as one document, i.e. not .spec file). Is this sufficient?
| class _PutBufferTemplate(BaseModel): | ||
| name: str = Field(description="Unique buffer name (also its on-disk spec stem).") | ||
| cvl: str = Field(description="The buffer's full CVL text (rules, methods{}, imports).") | ||
| property_rules: dict[str, list[str]] = Field( | ||
| default_factory=dict, | ||
| description="The properties this buffer verifies and, for each (by its snake_case title), the " | ||
| "rule/invariant names in this buffer's CVL that verify it. Across all run-target buffers every " | ||
| "non-skipped property must appear in exactly one buffer. Omit for a shared buffer.", | ||
| ) | ||
| is_run_target: bool = Field( | ||
| default=True, description="False for a shared, imported-only buffer that runs no rules." | ||
| ) | ||
|
|
||
|
|
||
| def put_buffer[S: WithBuffers](ty: type[S]) -> BaseTool: | ||
| schema = create_model( | ||
| "PutBuffer", __base__=_PutBufferTemplate, __doc__=put_buffer_description, | ||
| state=(Annotated[ty, InjectedState], ...), | ||
| tool_call_id=(Annotated[str, InjectedToolCallId], ...), | ||
| ) | ||
|
|
There was a problem hiding this comment.
turns out you can subscript generic pydantic models with concrete types just fine, so this create model template dance is totally unnecessary.
| def put_buffer(**args) -> str | Command: | ||
| if (err := cvl_syntax_error(args["cvl"])) is not None: | ||
| return err | ||
| buffers_now = args["state"].get("buffers") or {} |
There was a problem hiding this comment.
I guess ... what's the point of the argument schema if you're gonna throw it all away at the argument typing level? But with the above understanding, just use the "WithImplementation" and what not to avoid all this boilerplate.
| return await judges.for_buffer(name, properties)( | ||
| snap, spec, skipped, self.rebuttals, self.tool_call_id | ||
| ) |
There was a problem hiding this comment.
doesn't this mean every rebuttal goes to every feedback agent? even the ones not being rebutted?
| judge_host = _LiveJudgeHost(env, editing) | ||
| source_judges = _PerBufferJudge( | ||
| build=lambda name, claimed: source_feedback_judge( | ||
| judge_ctx.child(CacheKey[CVLJudge, CVLJudge](name)), judge_host, judge_prompt, claimed | ||
| ), | ||
| properties=props, | ||
| ) |
There was a problem hiding this comment.
given that we've dropped the structural invariant phase, which was the only user of this code that kept its source immutable, I don't see a particularly compelling reason to keep supporting a feature no one is using. I suspect it will make the footprint of this change much, much nicer; no more different mode juggling?
| ) | ||
| existing = buffers_now.get(args["name"]) | ||
| existing = buffers_now.get(self.name) | ||
| # Keep the prior property->rule mapping when the agent re-puts text without restating it. |
There was a problem hiding this comment.
is this mentioned in the tool documentation? I didn't see it.
| buffer is unchanged. Dramatically cheaper than `put_buffer` for a small change. | ||
| """ | ||
| def put_buffer[S: WithBuffers](ty: type[S]) -> BaseTool: | ||
| return tool_display_of(_put_display)(PutBuffer[ty].as_tool("put_buffer")) |
There was a problem hiding this comment.
does the annotation form not work? how strange!
| digests — the same runs :func:`buffer_is_complete` considers. Rule-striping runs one buffer's rules | ||
| across several jobs, so its verdicts are spread over all of these links rather than carried by the | ||
| last one alone.""" |
| ) -> Iterator[dict[str, str]]: | ||
| """Write every buffer as ``{name}__{tag}.spec`` into the specs dir (all at once, so any buffer's | ||
| ``import "<sibling>.spec"`` — retargeted to the tagged name — resolves), and yield ``name -> on-disk | ||
| spec path``; every file is removed on exit. The ``tag`` (unique per submission) isolates concurrent | ||
| jobs that share one run-root: on the in-situ path the run-root is the shared project directory, so | ||
| two jobs writing the deterministic ``{name}.spec`` would clobber each other and race on cleanup.""" | ||
| names = list(buffers) | ||
| """Write every buffer as ``{name}.spec`` into the specs dir (all at once, so any buffer's | ||
| ``import "<sibling>.spec"`` resolves to its sibling), and yield ``name -> on-disk spec path``; | ||
| every file is removed on exit. The run owns its materialized project folder, so the deterministic | ||
| filenames never collide with a concurrent job's.""" | ||
| with ExitStack() as stack: |
| @@ -637,6 +712,9 @@ class _BufJob: | |||
| #: so a job whose digest is now stale (its buffer or a shared import changed) can't mark it done. | |||
| digest: str | |||
| task: "asyncio.Task[None]" | |||
There was a problem hiding this comment.
unclear why this is quoted by okay
| **Strongly prefer splitting, and add over-approximating performance summaries preemptively.** A | ||
| single spec has ONE global `methods{}` block, so every rule is verified under the *intersection* of | ||
| what all rules need precise — one property that needs an expensive function kept exact forces EVERY | ||
| rule to pay that cost, which is the usual source of a timeout. Splitting breaks that coupling: each |
There was a problem hiding this comment.
I think you can trim this to be honest. You don't need to argue why splitting is expensive, fine to just say what splitting buys you.
| VIOLATED, analyze the cex: if it hinges on behavior your summary allows but the real function forbids, | ||
| it is spurious → tighten that summary (add the missing constraint) or drop the over-approximation for | ||
| that function with `edit_buffer`, then re-`submit_buffer`. Start from the | ||
| simplest sound over-approximation and tighten only as spurious cexes force you to. |
There was a problem hiding this comment.
there is a section in the context doc you can ref here I think
| verdict = await self._review( | ||
| b.name, buffer_review_text(buffers, b.name), skipped, claimed | ||
| ) | ||
| blocks.append(f"=== buffer {b.name} ===\nGood? {verdict.good}\nFeedback {verdict.feedback}") |
There was a problem hiding this comment.
does this mean skipped is evaluated against every buffer? and changing a skip will invalidate all buffers? I'm not mad about this, just making sure I understand.
2 participants
Summary
Today the CVL-generation agent authors one spec with one global
methods{}block, soevery rule is verified under the intersection of what all rules need precise — one property
that needs an expensive function (nonlinear math, hashing, a heavy external) kept exact forces
every rule to pay that cost. That coupling is a common source of timeouts, and a single
combined run cannot escape it.
This PR replaces the single-spec model with named spec buffers: the agent partitions its
properties into several self-contained CVL buffers, each with its own
methods{}(so afunction summarized in one buffer can stay exact in another), and each verified and reviewed
independently and in parallel. A function's precision cost is now paid only by the buffer that
needs it.
It also converts the prover interaction from a blocking, one-spec-at-a-time call into an
async submit/collect model, so buffers prove concurrently and the agent keeps working
(authoring the next buffer, or processing a finished result) instead of blocking on the slowest
job.
Validated end-to-end on a real project (see Validation).
The buffer model
put_buffer/edit_buffer/get_buffer/list_buffers/delete_bufferauthor CVL buffers;submit_buffer/collect_resultsverify them (replacingverify_spec).property_rules(the properties itverifies + their rule names) and is run by the prover. A shared buffer (
is_run_target=false)carries infrastructure (ghosts, common invariants, helper CVL, token/oracle models, summaries)
and is never run itself.
a subset of run-targets can share one base while another subset shares a different one, and
editing a shared buffer re-verifies only its importers.
and each rule lives in exactly one buffer (
validate_coverage/validate_disjoint_rules).feedback stamp keyed to a content digest over the buffer's import closure — so editing a
buffer (or a shared buffer it imports) invalidates exactly the buffers affected, and nothing
else is re-run.
The async prover model
submit_buffer(name)launches a prover job in the background and returns immediately(concurrency-throttled; idempotent; supersedes a stale in-flight job for the same buffer).
collect_results()drains finished jobs without blocking and returns a status board(
complete/running/needs (re)submission); it blocks only when there is nothing else todo. The agent works a strict priority order — process a finished result, else author/submit the
next buffer, else block on the next completion.
{name}__{digest}.specfiles with sibling imports retargeted, so concurrent jobs never read each other's in-flight
edits.
already-verified ones); the board lists them under
needs (re)submissionso the agent re-runsexactly those.
Guidance & advisories
splitting by precision need + adding over-approximating performance summaries preemptively
(before a monolithic run), including the
assert-only vssatisfysoundness split. It is arecommendation, not a mandate.
methods{}/ghost declarations duplicatedverbatim across run-targets and suggests hoisting them into a shared buffer. It only tells —
it never blocks.
Reliability fixes (independent; bundled here — can be split if preferred)
composer/llm/anthropic.py): a mid-stream connection dropsurfaces as a raw
httpx.RemoteProtocolError; treat it as retryable.composer/prover/cloud.py): a transient failure whiledownloading a completed job's results used to bubble up and re-run the whole (often
hours-long) proof. Now the fetch itself is retried with capped exponential backoff against the
already-
SUCCEEDEDjob.certora_autosetup/setup/sanity.py):AUTOPROVER_SANITY_TIMEOUT(default 1200s) caps the sanity phase's per-job timeout.
Config knobs
AUTOPROVER_MAX_SPEC_BUFFERS— max run-target buffers (default 6).AUTOPROVER_SANITY_TIMEOUT— sanity-phase per-job timeout in seconds (default 1200).Files
New substrate & tools:
composer/spec/source/spec_buffers.py— pure buffer substrate (model, import closure, digests,coverage/disjointness validation, completion stamps, dup detection).
composer/spec/source/buffer_tools.py— the authoring tools (put/get/edit/list/delete_buffer,cap enforcement).
Wiring & orchestration:
composer/spec/source/prover.py— asyncsubmit_buffer/collect_results, materialization,job supersession, dup-linter surfacing.
composer/spec/source/author.py— buffer-only authoring mode, per-buffer review/feedback,buffer guidance.
composer/spec/source/pipeline.py,autoprove_common.py,composer/spec/cvl_generation.py,composer/certora_env.py,certora_autosetup/cache/content_cache.py— supporting wiring.composer/templates/property_generation_system_prompt.j2— prompt updates.Testing
51 new unit tests across 7 files, all pure (no live prover / no jar):
test_spec_buffers.py(26) — substrate: ownership, import closure, digests, coverage,disjoint rules, completion stamps, dup detection, buffer-map reducer.
test_buffer_completion.py(6),test_spec_buffer_prover.py(5),test_buffer_tools.py(5) —completion tracking, async submit/collect + per-buffer feedback, cap enforcement.
test_cloud_fetch_retry.py(2),test_sanity_timeout.py(4),test_anthropic_retry.py(3) —the reliability fixes.
Full non-expensive suite green (1219 passed; the only errors are pre-existing
test_rag_db.py [postgres]env cases that need the local RAG container).pyrightclean.Validation (live cloud run)
Run on a testing real project:
init/ownership, impl/upgrade-auth, attack-vectors; combinatorial-collateral: core, operations,
attack) — i.e. multiple buffers within a property class, not merely one per class.
buffers were refined.
expected-failure attack vectors + refinement CEXes).
owner()across the 3 buffers) and the agentcorrectly treated it as a non-blocking suggestion.
same volume that previously surfaced transient stalls).
Follow-ups (out of scope)
spec_buffers.py): a pure-comment edit changes thebuffer digest and re-runs an identical proof. The fix is a separate comment-stripped prover
digest distinct from the raw feedback digest — noted, not done here.
custom_summaries.spec(SafeTransferLib path not covered) and the summarizer↔CVL-agentone-way handoff — a pre-existing, unrelated issue, not introduced by this PR; handed off
separately.